Nuprl Lemma : band_ff_simp
12,41
postcript
pdf
u
:
. (
u
ff) = ff
latex
ProofTree
Definitions
t
T
Lemmas
bool
wf
,
bfalse
wf
origin
u:
. (u 
ff) = ff 
u:. (u ff) = ff
T